| Definitions | x:A B(x), P & Q, A & B, {i..j },  x:A. B(x),  x:A. B(x), FairFifo, World, t  T, E, isrcv(k), P   Q, time(e), loc(e), a(i;t), kind(e), lnk(k), isrcv(l;a),  b, act(e), {x:A| B(x) }, False,  A,  , A B,  ,  ,  b, s = t, Prop, x:A  B(x), P  Q, Unit, left+right, a = b, p  q, True,  T, SqStable(P), kind(a), isnull(a), P Q, a<b, rcvs(l;t), ||as||, snds(l;t), Void,  x:A. B(x), Msg, S  T, #$n, Action(i), queue(l;t), Top, type List, i j, Type, ij, n-m, i<j, hd(l), msg(a), {T}, SQType(T), s ~ t, match(l;t;t'), IdLnk, i j < k, n+m,  x.A(x), x. t(x), l[i], w.M, mlnk(m), Id, Msg(M), source(l), m(i;t), onlnk(l;mss), concat(ll), upto(n), m(l;t), map(f;as), <a,b>, true, -n |
| Lemmas | select upto, map select, firstn map, firstn upto, bnot of le int, length upto, map length, select concat, concat wf, map wf, w-ml wf, upto wf, w-m wf, Msg wf, w-onlnk wf, Id wf, lsrc wf, mlnk wf, w-M wf, select wf, exists functionality wrt iff, assert of band, and functionality wrt iff, int seg wf, IdLnk wf, w-msg wf, nth tl decomp, general length nth tl, assert of lt int, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, le int wf, ge wf, non neg length, length wf1, w-action wf, w-rcvs wf, le wf, nat wf, w-snds wf, w-Msg wf, top wf, w-loc wf, w-time wf, assert-eq-lnk, sq stable from decidable, decidable assert, band wf, eq lnk wf, lnk wf, w-isnull wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, w-kind wf, w-a wf, bool wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, w-E wf, world wf |